$\forall$$r$:$\mathbb{N}$, $L$:(Top List). $\parallel$nth\_tl($r$;$L$)$\parallel$ = if $r$ $<$z $\parallel$$L$$\parallel$ then $\parallel$$L$$\parallel$ {-} $r$ else 0 fi $\in$ $\mathbb{Z}$